00100	Partial Function Logic and Its Applications
00200	
00300	  by Zohar Manna and John McCarthy
00400	
00500	
00600	ABSTRACT:  Several variants (most old) of the first
00700		   order logic of partial functions and 
00800		   predicates are described.  Some meta-theorems
00900		   are proved.  Applications are given to proving
01000		   the termination and equivalence of computation
01150		   processes and to formulating a theory of truth
01200	           and set theory without the usual restrictions.
01300	
01350	1. Introduction
01400		A partial function on a domain has a value only
01500	for some of its arguments; for other arguments it may have no
01600	value.  If the partial function  f  has a value at argument
01700	a  we say that  f(a)  is defined and write  *f(a).  Functions
01800	of several arguments are treated similarly and so are
01900	predicates - i.e., functions taking the values true and false.
02000	We include as limiting cases of partial functions, total
02100	functions defined for all arguments as well as the partial
02348	function undefined for all arguments.
02350	
02400		Partial functions arise naturally in connection
02500	with computation because a computing process may give a
02600	result for some arguments and for others run on indefinitely.
02700	Any attempt to get rid of the theory of partial functions
02800	and keep all the total computable functions fails because
02900	it is undecidable whether a function is total or even whether
03000	it is defined for particular arguments.
03100	
03200		This circumstance suggests studying a first order
03300	logic of partial functions and predicates analogous to 
03500	the usual first order logic of total functions and predicates.
03600	Partial functions defined by computing processes can be
03700	substituted for the function letters of this calculus in
03800	valid formulas and derivations without having either to 
03900	first prove them total or extend them to total functions 
04000	by some convention.  This has turned out to be useful in
04100	proving the equivalence of different computation processes
04200	and in proving that they do or do not terminate for a given
04300	class of arguments.
     

04350	
04400		To our knowledge there are three papers (Wang 1961),
04500	(McCarthy 1963), and (Hayes 1969) defining partial predicate
04600	calculi and two papers, (Manna and Pnueli 1968a) and (Manna
04700	and Pnueli 1968b) applying the calculus to proving termination
04800	(also called convergence) of computable functions.  We shall
04900	explain these calculi presently and unfortunately will have
05000	to define at least two more variants in this paper for a
05100	new field of application.
05200	
05300		The new applications result from the fact that not 
05400	all sentences of a partial function logic have truth values.
05600	Some do, some don't, some provably do, some provably don't,
05700	and whether a sentence has a truth value is in general 
05800	undecidable.  This allows us to make consistent formal
05900	systems containing self-referential sentences like those of
06000	natural language.  In particular, the truth of sentences can
06100	be axiomatized in partial function logic in such a way that
06200	sentences resembling "This sentence is false" are in the
06300	language but don't lead to contradiction because they
06400	have no truth values.
06500	
06600		In fact, we contend that natural languages should 
06800	be regarded as partial function languages in which not all
06900	sentences have truth values.  This casts doubt on prevalent
07000	doctrine that natural language is inherently contradictory 
07100	or at least inherently far from any formal language.  In
07200	particular we doubt the opinion of Tarski (1931) that an
07300	adequate treatment of truth requires a hierarchy of languages.
07500	
07600		Another possible application of partial function logic
07700	is to set theory although this is not yet worked out.  It
07800	seems that a partial function logic formulation of set theory
07900	need impose no restriction on the comprehension axiom
08000	for forming sets.  The set terms that give trouble
08050	either are not defined or the membership relation that gives
08075	rise to contradiction is undefined.  The usual proofs of
08175	contradiction simply turn into proofs that these particular
08275	terms are undefined.
     

08300	
08400		The final application we shall mention is getting a
08500	language for the "reasoning program" required by one approach
08600	to the artificial intelligence problem.  In fact, the idea that
08800	partial function logic has applications beyond the theory of
08900	computation arose in connection with an attempt to formalize
09000	knowledge of a term or a sentence and to avoid the paradoxes
     

00100	PROBLEMS TO SOLVE TO FINISH THIS PAPER
00200	
00300	1. Correct references so as to acknowledge Bochvar and others.
00400	
00500	2. Get rules of inference for partial propositional
00600	calculus complete in the sense that all valid
00700	deductions can be made.
00800	
00900	3. Get definitions of  true  , defined , and  value  for
01000	expressions.  
01100	
01200	4. Relate the extensive and the intensive forms 
01300	of defined.
01400	
01500	5. What about set theory.  Can we rehabilitate Frege
09100	described in (Kaplan and Montague 1960).